nLab Peter Dybjer

• webpage

Selected writings

Introducing the notion of inductive types and inductive families in type theory:

• Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 [doi:10.1017/CBO9780511569807.012, pdf]

• Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 [doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf]

On categorical models of dependent types:

• Peter Dybjer, Internal type theory, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci. 1158 Springer (1996) 120-134 [doi:10.1007/3-540-61780-9_66, pdf, MR1474535]

Generalization of inductive types to inductive-recursive types:

• Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 [doi:10.2307/2586554, pdf]

• Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) [doi:10.1007/3-540-45504-3_7, pdf]

For moree see:

• Peter Dybjer, Inductive and inductive-recursive definitions in type theory (link list)

On internal type theory:

• Peter Dybjer, Internal type theory, in: Types for Proofs and Programs, Lecture Notes in Computer Science 1158 (1996) 120-134 [doi:10.1007/3-540-61780-9_66, pdf]

On the categorical semantics of W-types by initial algebras over an endofunctor:

• Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 [doi:10.1016/S0304-3975(96)00145-4]

On the categorical model of dependent types by locally cartesian closed categories:

• Pierre Clairambault, Peter Dybjer, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, in Typed lambda calculi and applications, Lecture Notes in Comput. Sci. 6690 Springer (2011) [arXiv:1112.3456, doi:10.1007/978-3-642-21691-6_10]

category: people